{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,
  FlexibleContexts, ScopedTypeVariables, FlexibleInstances,
  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}

{- |

Module      :  Type.Yoko.SetModel
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Sets of types.

-}

module Type.Yoko.SetModel where

import Type.Yoko.Type

infix 0 :::
-- | A /type set model/ determines a set of types; /open/ or /closed/. @(:::)@
-- is comparable to the @Sat@ class (e.g. from @SYB3@).
class (True ~ (a ::? u)) => a ::: u where membership :: u a



-- | The @::?@ type family realizes type-level predicates (over types) that
-- yield a type-level Boolean: either 'True' or 'False'. For type sets, it is a
-- /conservative/ approximation of inhabitance.
infix 0 ::?
type family a ::? (u :: * -> *)


-- | Most @SetModel@s can "reprove" the corresponding @:::@ constraint to the
-- type-checker.
class SetModel u where evidence :: u a -> ((a ::: u) => b) -> b

infix 3 :=>
class u :=> v where weaken :: u a -> v a
weakenTo :: (u :=> v) => [qP|v :: *->*|] -> u a -> v a
weakenTo _ = weaken



type family WitnessBT (u :: * -> *) (v :: * -> *)

data NoWitness (u :: * -> *) (v :: * -> *)
type Witness u v = FromMaybe (NoWitness u v) (WitnessBT u v)

type SuchThat (u :: * -> *) (v :: * -> *) = (u (Witness u v), v (Witness u v))
witness :: (Witness u v ::: u, Witness u v ::: v) => [qP|v :: *->*|] -> SuchThat u v
witness _ = (membership, membership)



-- | @(:?)@ helps us write /guarded/ @(:::)@ instances (see
-- <http://hackage.haskell.org/trac/ghc/ticket/5590>)
infix 1 :?
data (u :? anno) a = Anno (u a)


-- | For use with @(:::)@ instances that use @(:?)@.
membershipAnno :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a
membershipAnno _ = i where Anno i = membership :: (u :? anno) a

-- | Sometimes it's helpful to specify which @t@ must be in the type set.
membershipFor :: (t ::: u) => [qP|t|] -> u t
membershipFor _ = membership

-- | Sometimes it's helpful to specify which @u@ it is that @t@ must inhabit.
membershipIn :: (t ::: u) => [qP|u :: *->*|] -> u t
membershipIn _ = membership

-- | Returns a proxy for the is inhabiting the type set.
elemProxy :: u t -> [qP|t|];   elemProxy _ = infP


-- | The set of all types; it has /no/ contraints.
data NoneU a = NoneU
type instance t ::? NoneU = True
instance SetModel NoneU where evidence _ x = x
instance a ::: NoneU where membership = NoneU

type Both = (:&&)
infixr 3 :&&
-- | SetModel product.
data (u :&& v) a where (:&&) :: u a -> v a -> (u :&& v) a
type instance a ::? (u :&& v) = And (a ::? u) (a ::? v)
instance (SetModel u, SetModel v) => SetModel (u :&& v) where
  evidence (u :&& v) x = evidence u $ evidence v x
instance (a ::: u, a ::: v) => a ::: u :&& v where
  membership = membership :&& membership



instance (a ~ b, EQ ~ Compare a a) => b ::: (:=:) a where membership = Refl
instance (EQ ~ Compare a a) => SetModel ((:=:) a) where evidence Refl x = x
type instance t ::? ((:=:) a) = IsEQ (Compare a t)
instance (a ::: v) => ((:=:) a) :=> v where weaken Refl = membership

type instance WitnessBT ((:=:) t) p = If (t ::? p) (Just t) Nothing



infixr 2 :||
-- | SetModel sum.
data (u :|| v) a where
  LeftU  :: u a -> (u :|| v) a
  RightU :: (False ~ (a ::? u)) => v a -> (u :|| v) a

instance (EqT u, EqT v) => EqT (u :|| v) where
  eqT (LeftU uL) (LeftU uR) = eqT uL uR
  eqT (RightU vL) (RightU vR) = eqT vL vR
  eqT _ _ = Nothing

instance (u :=> w, v :=> w) => (u :|| v) :=> w where
  weaken u = case u of LeftU u -> weaken u; RightU v -> weaken v

instance (SetModel u, SetModel v) => SetModel (u :|| v) where
  evidence u x = case u of
    LeftU u -> evidence u x;   RightU u -> evidence u x

instance (anno ~ (a ::? u), a ::: u :|| v :? anno
         ) => a ::: u :|| v where membership = membershipAnno [qP|anno|]
instance (a ::: u) => a ::: u :|| v :? True where
  membership = Anno $ LeftU membership
instance (False ~ (a ::? u), a ::: v) => a ::: u :|| v :? False where
  membership = Anno $ RightU membership



type instance t ::? ((u :|| v) :? branch) = t ::? (u :|| v)

type instance t ::? (u :|| v) = Or (t ::? u) (t ::? v)


type instance WitnessBT (u :|| v) w =
  MaybePlus (WitnessBT u w) (WitnessBT v w)



-- | The empty set.
data VoidU t



type instance t ::? u :. f = f t ::? u
instance (f t ::: u) => t ::: u :. f where membership = Compose membership
instance SetModel u => SetModel (u :. f) where
  evidence (Compose u) x = evidence u x





-- | Finite type sets can be represented as type-sums.
type family Fin (u :: * -> *) :: * -> *
class Finite (u :: * -> *) where
  toFin :: u t -> Fin u t
  predFin :: [qP|u :: * -> *|] -> [qP|t|] -> (((t ::? u) ~ (t ::? Fin u)) => a) -> a

-- | @frFin@ sometimes requires a stronger context than does @frFin@, so we
-- separate the two methods.
class Finite u => Etinif u where frFin :: Fin u t -> u t

membershipFin :: (a ::: Fin u, Etinif u) => u a
membershipFin = frFin membership

-- | Any finite set can be used to determine type equality.
eqTFin :: (EqT (Fin u), Fin u ~ Fin v, Finite u, Finite v
          ) => u a -> v b -> Maybe (a :=: b)
eqTFin x y = eqT (toFin x) (toFin y)

-- | Finite sets can be weakened by enumeration.
weakenFin :: (Fin u :=> v, Finite u) => u a -> v a
weakenFin = weaken . toFin

type WitnessBTFin (u :: * -> *) (v :: * -> *) = WitnessBT (Fin u) v
